\section{Herbrandova veta - história}
\startFIXME
\par Leibniz (1646 -- 1716), Peáno (1900), Hilbertova škola (1920), Herbrand
(1930). Fundamentálny výsledok, ktorý dal odpoveď na otázku, či existuje
všeobecná procedúra, ktorá vie zistiť, či je daná formula tautológia, dali
Church a Turing (1936, nezávisle od seba) -- ukázali, že v predikátovej logike
nie je problém rozhodnuteľnosti riešiteľný.
\par Herbrandova metóda je založená na procedúre vyvrátenia. Ide o nájdenie
interpretácie, pri ktorej daná formula nie je splnená. Ak formula nie je
tautológia, v konečnom počte krokov sa procedúra zastaví, pokiaľ ale nie je,
procedúra pokračuje vo výpočte.

\par Gilmore (1960), Davis a Putnem (1960) -- navrhovali procedúry, ktoré by
boli schopné overovať tautologickosť formúl; fungovali ale iba pre jednoduchšie
formuly.

\par V rokoch 1965 -- 1968 Robinson zaviedol pojem \emph{resolventa} (v podstate
iným spôsobom zapísane pravidlo \emph{modus ponens}.
\stopFIXME
